T:Type, R, R':(TT).
(x, y:T. {R(x,y)  R'(x,y)})  {Connex(T;x,y.R(x,y))  Connex(T;x,y.R'(x,y))} 

latex

ProofTree

Definitions	t  T, P  Q, Connex(T;x,y.R(x;y)), x(s1,s2), {T}, P  Q, , x:A. B(x), x. t(x), x(s)
Lemmas	or functionality wrt implies, all functionality wrt implies